RCS "$Id: PolyGraph.sig,v 1.10 1998/08/13 11:35:06 pxs Exp $";
(*********************************** Graph ***********************************)
(*                                                                           *)
(* Generation of polygraphs.                          Joachim Parrow June-88 *)
(*                                                                           *)
(* States in a graph are maintained in decreasing order with respect to      *)
(* their id's. This is true also of the suc, taus and newtaus fields, and    *)
(* the suc lists are maintained sorted according to their actions.           *)
(*                                                                           *)
(* reflexcl: takes a graph and adds tau loops to all states.                 *)
(* transcl: Replaces -tau-> with the transitive closure of -tau->.           *)
(* actcl: Adds (-tau->* -a->* -tau->) to -a->. This will only work on a      *)
(*    graph which has been produced by "transcl".                            *)
(* obscl: The three above graph transformations are effected.                *)
(* congrcl: This graph transformation goes with the bisimulation algorithm.  *)
(*    to check for observation congruence. replicates initial state and does *)
(*    NOT add a tau loop on the initial state.                               *)
(* epscl: Adds epsilon loop to the initial state of the graph.               *)
(*                                                                           *)
(*****************************************************************************)

signature POLYGRAPH =
sig
  structure Ag : AGENT_WRAPPER
  type '_a graph

  datatype 'a state =
    S of {keycopy  : Ag.agent ref,	
	  id       : int,
	  suc      : (Ag.A.act * 'a state ref list ref) list ref,
	  prdiv    : bool,
	  gldiv    : bool ref,
	  info     : 'a,
	  taus     : 'a state ref list ref,
	  newtaus  : 'a state ref list ref,
	  tauarr   : bool Array.array ref,
	  mark     : bool ref,
	  p_id     : int ref}

   exception LookUp

   val mkgraph     :  
       (Ag.agent -> '_a) ->                                  (* poly init     *)
       (Ag.agent -> bool) ->                                 (* divergence fn *)
       (Ag.agent -> Ag.agent) ->                                (* normalform fn *)
       (Ag.agent -> (Ag.A.act * Ag.agent) list) ->                   (* transition fn *)  
       Ag.agent -> '_a state ref * '_a state ref list

(* same as above, bar type -- beginning of long encapsulation process *)
   val makegraph     :  
       (Ag.agent -> '_a) ->                                  (* poly init     *)
       (Ag.agent -> bool) ->                                 (* divergence fn *)
       (Ag.agent -> Ag.agent) ->                                (* normalform fn *)
       (Ag.agent -> (Ag.A.act * Ag.agent) list) ->                   (* transition fn *)  
       Ag.agent -> '_a graph

   val mkweakgraph :  
       (Ag.agent -> '_a) ->                                  (* poly init     *) 
       (Ag.agent -> bool) ->                                 (* divergence fn *)
       (Ag.agent -> Ag.agent) ->                                (* normalform fn *)
       (Ag.agent -> (Ag.A.act * Ag.agent) list) ->                   (* transition fn *)  
       Ag.agent -> '_a state ref * '_a state ref list

   val makeweakgraph :  
       (Ag.agent -> '_a) ->                                  (* poly init     *) 
       (Ag.agent -> bool) ->                                 (* divergence fn *)
       (Ag.agent -> Ag.agent) ->                                (* normalform fn *)
       (Ag.agent -> (Ag.A.act * Ag.agent) list) ->                   (* transition fn *)  
       Ag.agent -> '_a graph

   val reflexcl  : '_a state ref * '_a state ref list -> 
                   '_a state ref * '_a state ref list
   val transcl   : '_a state ref * '_a state ref list -> 
                   '_a state ref * '_a state ref list
   val actcl     : '_a state ref * '_a state ref list -> 
                   '_a state ref * '_a state ref list
   val obscl     : '_a state ref * '_a state ref list -> 
                   '_a state ref * '_a state ref list
   val congrcl   : '_a -> '_a state ref * '_a state ref list -> 
                   '_a state ref * '_a state ref list
   val epscl     : '_a state ref * '_a state ref list -> 
                   '_a state ref * '_a state ref list
(* for migration to sensible data structures! *)
   val wrapUp : '_a state ref * '_a state ref list -> '_a graph
(* ******************************************************************** *)
(* functions for manipulating successor lists, which preserve orderings *)
(* ******************************************************************** *)
(* the lists you pass in can be unsorted *)
   val setSuccessors : '_a state ref *
     (Ag.A.act * '_a state ref list ref) list -> unit

(* add to the given state the info that via action you can reach the states *)
(* in newVal, in addition to whatever we knew we could do. *)     
(* the list you pass in can be unsorted *)
   val addActionSuccessors : '_a state ref * Ag.A.act * '_a state ref list -> unit

(* action list must be sorted *)
   val removeActionSuccessors : '_a state ref * Ag.A.act list -> unit

   val setTausFromSuccessors : '_a state ref -> unit

   val getActionSuccessors : '_a state ref * Ag.A.act -> '_a state ref list

  val SGraph : (Ag.agent -> '_a) -> Ag.agent ->
    '_a state ref * '_a state ref list
  val PSGraph : (Ag.agent -> '_a) -> Ag.agent -> '_a graph
  val WGraph : (Ag.agent -> '_a) -> Ag.agent ->
    '_a state ref * '_a state ref list
  val PWGraph : (Ag.agent -> '_a) -> Ag.agent -> '_a graph
end

